x, tg:Id, k:Knd, l:IdLnk, T, A, B:Type.
(rcv(l,tg) = k  T = B)
 (f:(ABT), c:(AB).
 (@source(l): k(v) sends [tg,   a,b. if c(a,b) [f(a,b)] else nil fi(x, v)] on link l    Dsys
 (& (D:Dsys.
 (& (@source(l): k(v) sends [tg,   a,b. if c(a,b) [f(a,b)] else nil fi(x, v)] on link l    D
 (& ( D 
 (& ( realizes es.
 (& ( vartype(source(l);x)  A
 (& ( & (e:E. loc(e) = source(l)  Id  kind(e) = k  Knd  valtype(e)  B)
 (& ( & (e:E. kind(e) = rcv(l,tg)  Knd  valtype(e)  T)
 (& ( & (e:E.
 (& ( & (loc(e) = source(l)  Id
 (& ( & ( kind(e) = k  Knd
 (& ( & ( (c((x when e),val(e))
 (& ( & ( ( (e':E.
 (& ( & ( ( (kind(e') = rcv(l,tg)  Knd
 (& ( & ( ( (& sender(e') = e  E
 (& ( & ( ( (& & (e'':E.
 (& ( & ( ( (& & (kind(e'') = rcv(l,tg)  Knd  sender(e'') = e  E  e'' = e'  E)
 (& ( & ( ( (& & val(e') = f((x when e),val(e))  T))
 (& ( & ( & (c((x when e),val(e))
 (& ( & ( & ( (e':E. kind(e') = rcv(l,tg)  Knd & sender(e') = e  E))))) 

latex

Definitions

, AB, hd(l), (x  l), P  Q, sender(e), ij, Top, ||as||, P  Q, SQType(T), {T}, P  Q, x when e, vartype(i;x), ES, T, True, val(e), valtype(e), b, b, A, False, x:A. B(x), if b t else f fi, IdLnk, rcv(l,tg), , D realizes es. P(es), Dsys, D1  D2, World, FairFifo, PossibleWorld(D;w), A & B, E, Id, loc(e), source(l), P & Q, Prop, Knd, kind(e), ES(the_w), x:A. B(x), P  Q, t  T

Lemmas

w-es wf, es-kind wf, Knd wf, lsrc wf, es-loc wf, Id wf, es-E wf, possible-world wf, fair-fifo wf, world wf, d-sub wf, dsys wf, ifthenelse wf, bool wf, rcv wf, IdLnk wf, s-sends-rule1, assert wf, not wf, bnot wf, es-vartype wf, subtype rel wf, es-val wf, es-when wf, assert of bnot, eqff to assert, iff transitivity, bool sq, eqtt to assert, bool cases, event system wf, true wf, squash wf, length-map, length wf1, non neg length, es-sender wf, member singleton, es-kind-rcv, ge wf, hd wf